Nuprl Lemma : imax_add_r
12,41
postcript
pdf
a
,
b
,
c
:
. imax(
a
;
b
)+
c
= imax(
a
+
c
;
b
+
c
)
latex
ProofTree
Definitions
True
,
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
bnot
wf
,
lt
int
wf
,
le
wf
,
assert
wf
,
bool
wf
,
le
int
wf
origin
a, b, c:
. imax(a;b)+c = imax(a+c;b+c)
a, b, c:. imax(a;b)+c = imax(a+c;b+c)
Tx:A. B(x)